es:ES, e2, e1:E.
e1  e2   (n:. 0<n  n<||[e1, e2]||  e(e1,e2].||[e1, pred(e)]|| = n  ) 

latex

Definitions

t  T, x:A. B(x), E, P & Q, P  Q, P  Q, ||as||, b, False, A, AB, , WellFnd{i}(A;x,y.R(x;y)), x,y. t(x;y), (e <loc e'), P  Q, first(e), , Prop, loc(e), Id, pred(e), 1of(t), [e, e'], x. t(x), e(e1,e2].P(e), e  e' , {T}, ES, A & B, Dec(P), ij, x:A. B(x), P  Q, Top, S  T, True, T

Lemmas

es-interval-eq, es-le-self, and functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, squash wf, true wf, es-interval-less, es-le-pred, length-append, es-interval wf2, top wf, decidable lt, es-pred-locl, es-le-iff, event system wf, es-locl-wellfnd, es-locl wf, es-le wf, nat wf, existse-between3 wf, length wf1, es-interval wf, es-pred wf, Id wf, es-loc wf, not wf, assert wf, es-first wf, es-le-loc, wellfounded functionality wrt iff, es-loc-pred, es-locl-iff, es-E wf